Cut Elimination

释义 Definition

（逻辑/证明论）割消去：指在序列演算等形式系统中，通过一系列变换把证明里使用的 cut（割）规则去掉，同时仍能证明同一个结论。直观上，它把“先引入一个中间命题再消去”的推理步骤改写为更“直接”的推导，常用于说明系统的一致性、可判定性、子公式性质等。该术语在更广义上也可指“消除中间引理式步骤”的证明正规化思想。

发音 Pronunciation (IPA)

/kʌt ˌɛlɪˈmeɪʃən/

例句 Examples

Cut elimination can simplify a proof by removing unnecessary intermediate steps.
割消去可以通过移除不必要的中间步骤来简化一个证明。

In sequent calculus, the cut elimination theorem shows that any proof using cut can be transformed into a cut-free proof, often yielding the subformula property.
在序列演算中，割消去定理表明任何使用割规则的证明都能转换为不含割的证明，并且往往由此得到子公式性质。

词源 Etymology

cut 在证明论里是“割规则”的名称（把一个中间公式当作“切口/接口”，把两段推导接起来）；elimination 来自拉丁语 eliminare，有“移出、去除”的意思。术语整体主要与德国逻辑学家 Gentzen（根岑）在 1930 年代提出的证明论工作相关，他用割消去来刻画证明的“正规化/纯化”。

相关词 Related Words

• Cut
• Sequent
• Sequent Calculus
• Proof Theory
• Normalization
• Consistency
• Subformula Property
• Gentzen

文学与名著中的用例 Literary Works

• Gerhard Gentzen, Investigations into Logical Deduction（1934–1935）：提出并系统讨论割消去思想（常与“割消去定理”相关联）。
• Gaisi Takeuti, Proof Theory：以“cut-elimination”作为证明论核心技术之一反复使用与推广。
• S. Troelstra & H. Schwichtenberg, Basic Proof Theory：在序列演算与自然演绎框架中讲解割消去与正规化的关系。
• Jean-Yves Girard, Proofs and Types：在类型论与证明论对应（Curry–Howard）背景下涉及相关正规化/消去结果。